|i| == if 0 z i then i else -i fi  

latex

Up	int 2, int 2
Wellformedness Lemmas	absval wf, absval wf
Definitions	if b then t else f fi , i z j, #$n, -n
FDL editor aliases	absval